\section{Substitúcia a unifikácia}

Vo výrokovej logike nebol problém hľadať kontrárne dvojice.
Zložitejšia situácia ale nastáva v prípade predikátovej logiky
prvého rádu. A práve tomu sa budeme venovať v tejto kapitole.
Uvažujme napríklad dve klauzuly
$C_1=P(x) \lor Q(x)$, $C_2 = \neg P(f(x)) \lor R(x)$.
V nich neexistuje žiadna kontrárna dvojica. Ak však nahradím premennú
$x$ za term $f(a)$ v prvej klauzule a za term $a$ v druhej klauzule,
dostaneme základné inštancie
$C_1'=P(f(a)) \lor Q(f(a))$, $C_2'=\neg P(f(a)) \lor R(a)$.
Teraz môžeme definovať rezolventu; bude to $Q(f(a)) \lor R(a)$.
Mohli by sme postupovať aj všeobecnejšie -- nahraďme $x$ za $f(x)$ v
prvej klauzule a dostávame
$ C_1^*= P(f(x)) \lor Q(f(x))$, $C_2^*= \neg P(f(x)) \lor R(x)$.

Rezolventa potom bude $C^*= Q(f(x)) \lor R(x)$.
Vidíme teda, že sme získali 2 rôzne rezolventy, jednu viac všeobecnú
ako druhú. No a práve v ďalšom texte si formálne zadefinujeme toto
dosadzovanie hodnôt a popíšeme spôsob, ako hľadať najvšeobecnejšie
rezolventy.

\begin{definicia}[Substitúcia]
    Pod substitúciou rozumieme konečnú množinu tvaru:
    $\{t_1/v_1, \ldots, t_n/v_n\}$, kde každé $v_i$ je premenná a
    $t_i$ je term.
    Ďalej požadujeme, aby všetky
    $v_i$ boli navzájom rôzne ($i \in\{1,\dots,n\}$)
    a aby term $t_i$ bol rôzny od $v_i$. Touto množinuo budeme
    popisovať činnosť ``naraz nahraď každú premennú $v_i$ termom $t_i$''.

    Ak $t_1, \ldots, t_n$ sú základné inštancie (teda termy bez premenných),
    tak substitúciu nazývame tiež základná substitúcia.
\end{definicia}

\begin{poznamka}
    Na označovanie substitúcií budeme používať grécke písmená.
    Špeciálne, prázdnu substitúciu označíme ako $\eps$.\footnote{
        Pozn.: Vzniká nám tu kolízia označenia s prázdnou nesplniteľnou
        klauzulou. Z kontextu však bude jasné, o ktorý prípad pôjde.
    }
\end{poznamka}

\begin{poznamka}
    Je dôležité si všimnúť, že poradie prvkov v definícii substitúcie je
    čisto antiintuitívne -- človek by očakával ``premenná/výraz ktorým ju
    máme nahradiť'' a nie ``výraz/premenná''.
\end{poznamka}

\begin{priklad}
    Jedna substitúcia môže byť napr.
    $\alpha = \{ f(z)/x,\ y/z\}$, teda $x$ nahrádzame za $f(z)$ a
    $z$ za $y$.
    Ďalšia môže byť $\beta = \{ a/x,\ g(y)/y,\ f(g(y))/z\}$.
\end{priklad}

\begin{definicia}
    Nech $\theta$ je ľubovoľná substitúcia a $E$ je nejaký výraz.
    Nech $\theta = \{ t_1/v_1, \dots, t_n/v_n\}$.
    Potom $E\theta$ označuje výraz, ktorý vznikne tak,
    že súčasne vo výraze $E$ nahradíme každý výskyt premenej $v_i$ termom $t_i$
    pre $i \in \{1,\dots,n\}$. Takýto výraz nazveme inštanciou $E$.
\end{definicia}

\begin{priklad}
    Majme substitúciu $\theta=\{a/x,\ f(b)/y,\ c/z\}$
    a výraz $E = P(x, y, z)$.
    Potom $E\theta = P(a, f(b), c)$.
\end{priklad}

\medskip
\noindent
Ďalšia operácia, ktorú budeme potrebovať, je operácia skladania
substitúcií.

\begin{definicia}[Kompozícia substitúcii]
    Majme substitúcie $\theta = \{t_1/x_1, \ldots t_n/x_n\}$ a
    $\lambda = \{ u_1/y_1, \ldots u_m/y_m \}$.
    Zloženie (kompozícia) $\theta \circ \lambda$ substitúcií
    $\theta,\lambda$ je definované ako množina
    \begin{equation*}
        \{t_1 \lambda/x_1, \dots, t_n \lambda/x_n, u_1/y_1, \dots, u_m/y_m \}
    \end{equation*}
    z ktorej navyše vyradíme všetky členy $t_i\lambda/x_i$,
    pre ktoré platí, že $t_i \lambda = x_i$ (aby sme nesubstituovali
    identititami)
    a tiež vyradíme všetky $u_i/y_i$,
    pre ktoré $y_i \in \{x_1, x_2, \dots, x_n\}$ (lebo by sme mali
    dvojité správanie sa substitúcie na $x_i$).
\end{definicia}

\begin{poznamka}
    Kompozícia $\theta \circ \lambda$ sa správa rovnako ako postupné
    aplikovanie $\theta, \lambda$. Čiže
    $E(\theta \circ \lambda) = (E\theta)\lambda$.
\end{poznamka}

\begin{priklad}
    Majme substitúcie
    \begin{align*}
        \theta = \{t_1/x_1,\ t_2/x_2\} = \{ f(y)/x,\ z/y\} \\
        \lambda = \{u_1/y_1,\ u_2/y_2,\ u_3/y_3\} = \{ a/x,\ b/y,\ y/z\}
    \end{align*}
    Potom
    \begin{equation*}
    \begin{split}
        \theta \circ \lambda &= 
            \{ t_1 \lambda / x_1,\ t_2\lambda/x_2,\
            u_1/y_1,\ u_2/y_2,\ u_3/y_3\} - \{\dots\} \\ 
        &= \{f(b)/x,\ y/y,\ a/x,\ b/y,\ y/z\} - \{y/y,\ a/x,\ b/y\} \\
        &= \{f(b)/x,\ y/z\}
    \end{split}
    \end{equation*}
\end{priklad}

\begin{poznamka}
    Skladanie substitúcií je asociatávna operácia, teda ak zoberieme 
    $\theta, \lambda, \mu$, potom platí 
    $\theta \circ(\lambda \circ \mu) = (\theta \circ \lambda) \circ \mu$.

    Tiež platí, že $\varepsilon \circ \theta = \theta = 
            \theta \circ \varepsilon$.
    To znamená, že množina substitúcii s operáciou skladania je
    pologrupa (monoid) s jednotkou.
\end{poznamka}

\begin{definicia}[Unifikátor]
    Substitúciu $\theta$ nazveme unifikátorom
    množiny výrazov $E_1, E_2, \dots, E_n$,
    ak platí $E_1\theta = E_2\theta = \cdots = E_n\theta$.
    Množinu nazveme unifikovateľnou, ak pre ňu existuje
    unifikátor, ktorý je zjednocuje.
\end{definicia}

\begin{priklad}
    Majme množinu $\{P(a,y),\ P(x,f(b)\}$.
    Potom jeden z možných unifikátorov je napríklad
    $\theta = \{a/x,\ f(b)/y\}$.
\end{priklad}

\begin{poznamka}
    Nie každá množina má unifikátor. Naopak, množina môže mať aj
    viacej unifikátorov. Vtedy má medzi nimi význačné miesto takzvaný
    najvšeobecnejší unifikátor.
\end{poznamka}

\begin{definicia}[Najvšeobecnejší unifikátor]
    Majme množinu výrazov $S=\{ E_1, E_2, \ldots, E_n\}$.
    Unifikátor $\sigma$ pre množinu výrazov $S$ nazveme 
    najvšeobecnejší unifikátor, ak pre ľubovoľný unifikátor $\theta$
    množiny $S$ platí, že existuje substitúcia 
    $\lambda_{\theta}$ taká, že $\theta = \sigma \circ \lambda_{\theta}$.
\end{definicia}

\medskip
Pri hľadaní unifikátorov budeme pozerať na rozdiely vo výrazoch.
Uvažujme napríklad výrazy $P(a)$, $P(x)$.
Pozerajme sa na ne ako na konečnú postupnosť symbolov -- 
odlišujú sa akurát v treťom symbole. Toto je prvá odlišnosť/diferencia.
Vo všeobecnosti môže byť týchto výrazov viacej a preto si zadefinujeme
diferenčnú množinu.

\begin{definicia}[Diferenčná množina]
Nech $W$ je neprázdna množina výrazov.
Diferenčnú množinu pre množinu výrazov $W$ dostávame tak, 
že na výrazy sa pozrieme ako na postupnosti symbolov, nájdeme prvú pozíciu
(zľava), na ktorej sa líšia a tieto rozdielne výrazy vypíšeme.
\end{definicia}

\begin{poznamka}[Nebolo na prednáške]
    Iný (a podľa mňa lepší) pohľad na to, ako získať diferenčnú množinu je
    pozrieť sa na stromy daných výrazov a začať ich naraz rekurzívne
    prehľadávať zľava doprava až narazíme na vrchol, ktorý je v niektorom
    výraze iný. Vtedy do diferenčnej množiny zoberieme pre každý výraz
    podstrom zakorenený v dotyčnom vrchole.
\end{poznamka}

\begin{priklad}
    \label{prikl:dif1}
    Majme množinu $W = \{P(x,f(y,z),\ P(x,a),\ P(x,g(h(k(x))))\}$.
    Nájdeme prvý pozíciu na ktorej sa líšia:
    $\{P(x,\underline{f(y,z)},\ P(x,\underline{\phantom{(}\!a}),\
    P(x,\underline{g(h(k(x)))}) \}$.
    Diferenčnou množinou bude množina líšiacich sa podvýrazov, teda
    $D= \{ f(y,z),\ a,\ f(h(k(x)))\}$. Jej grafická konštrukcia je na
    obrázku \ref{fig:dif1}.
    \begin{figure}[h]
        \centering
        \subfigure[$P(x,f(y,z))$]{
            \imageontop{
                \includegraphics[scale=0.8]{img/12/diferencia.1.mps}
            }
        }
        \subfigure[$P(x,a)$]{
            \imageontop{
                \includegraphics[scale=0.8]{img/12/diferencia.2.mps}
            }
        }
        \subfigure[$P(x,g(h(k(x))))$]{
            \imageontop{
                \includegraphics[scale=0.8]{img/12/diferencia.3.mps}
            }
        }

        \caption{Ukážka diferenčnej množiny z príkladu \ref{prikl:dif1}}
        \label{fig:dif1}
    \end{figure}
\end{priklad}

\begin{priklad}[Nebol na prednáške]
    \label{prikl:dif2}
    Uvažujme $W=\{P(a,f(a),f(g(y))),\ P(a,f(a),f(u))\}$.
    Diferenčná množina je $D=\{g(y),u\}$ a grafické znázornenie je na
    obrázku \ref{fig:dif2}.
    \begin{figure}[h]
        \centering
        \subfigure[$P(a,f(a),f(g(y)))$]{
            \imageontop{
                \includegraphics[scale=0.8]{img/12/diferencia.11.mps}
            }
        }
        \subfigure[$P(a,f(a),f(u))$]{
            \imageontop{
                \includegraphics[scale=0.8]{img/12/diferencia.12.mps}
            }
        }

        \caption{Ukážka diferenčnej množiny z príkladu \ref{prikl:dif2}}
        \label{fig:dif2}
    \end{figure}
\end{priklad}

\begin{poznamka}
    Do diferenčnej množiny zakaždým vyberáme iba jednu (prvú) nezhodu.
    Napríklad pre $W=\{P(x,y,z),\ P(y,f(a),g(x,y))\}$ je diferenčná množina
    iba $D=\{x,y\}$.
\end{poznamka}

\subsection{Unifikačný algoritmus}

Teraz si ukážeme jeden z algoritmov používaných na unifikáciu množiny. Bude
dookola opakovať nasledujúce kroky:
\begin{enumerate}
    \item na začiatku polož kolo $k=0$, množinu na unifikovanie 
        $W_0 = W$ a počiatočnú substitúciu  $\sigma_0 = \eps$.

    \item Ak $W_k$ obsahuje jedinú klauzulu,\footnote{Na prednáške
        to bolo ``obsahuje jednotkovú klauzulu'' ale toto označenie je
        mätúce.} algortimus zakončí svoju činnosť
        a $\sigma_k$ je najvšeobecnejší unifikátor.
        V opačnom prípade nájdeme diferenčnú množinu $D_k$ pre $W_k$.

    \item Ak existujú také elementy $v_k,t_k \in D_k$, že $v_k$ je
        premenná, ktorá sa nevyskytuje v terme $t_k$, tak pokračujeme ďalším
        krokom.
        V opačnom prípade algoritmus zakončuje svoju činnosť
        s výsledkom, že množina $W$ nie je unifikovateľná.

    \item Položme $W_{k+1} = W_k \{t_k/v_k\}$ a
        $\sigma_{k+1} = \sigma_k \circ \{t_k/v_k\}$. 

    \item pokračujeme krokom 2.
\end{enumerate}

\begin{poznamka}
    Ak je množina unifikovateľná, vždy existuje najvšeobecnejší unifikátor.
\end{poznamka}

\begin{priklad}
    Nájdite najvšeobecnejší unifikátor pre množinu
    \begin{equation*}
        W=\{ P(a,x,f(g(y))),\ P(z,f(z),f(u)) \}
    \end{equation*}

    Algoritmus bude pracovať nasledovne:
    \begin{enumerate}
        \item $\sigma_0 = \eps, W_0 = W$.

        \item Pretože $W_0$ obsahuje viac klauzúl klauzula,
            $\sigma_0$ nie je najvšeobecnejší unifikátor a pokračujeme
            vo výpočte.

        \item Zostrojíme diferenčnú množinu $D_0 = \{a, z\}$.
            Existuje premenná $v_0 = z$, 
            ktorá nie je obsiahnutá v terme $t_0 = a$.

        \item \itemMath{
            \begin{align*}
            \sigma_1 &= \sigma_0 \circ \{ t_0/v_0 \} = 
                \eps \circ \{a/z\} = \{a/z\}\\[5pt]
            \begin{split}
                W_1 &= W_0 \{ t_0/v_0 \} = 
                    \{P(a,x,f(g(y))),\ P(z,f(z),f(u))\} \{a/z\} \\
                    &= \{P(a,x,f(g(y))),\ P(a,f(a),f(u))\}
            \end{split}
            \end{align*}
            }

        \item $W_1$ neobsahuje jedinú klauzulu. Pokračujeme vo výpočte

        \item Zostrojíme diferenčnú množinu $D_1 = \{x, f(a)\}$.

        \item V $D_1$ máme premennú $v_1 = x$ a term $t_1 = f(a)$.

        \item \itemMath{
            \begin{align*}
            \sigma_2 &= \sigma_1 \circ \{ t_1/v_1\}= 
                \{a/z\} \circ \{ f(a)/x\} = \{a/z,\ f(a)/x \} \\[5pt]
            \begin{split}
                W_2 &= W_1 \{t_1/v_1\} = 
                    \{P(a,x,f(g(y))),\ P(a,f(a),f(u))\} \{f(a)/x\} = \\
                    &= \{ P(a,f(a),f(g(y))),\ P(a,f(a),f(u)) \}
            \end{split}
            \end{align*}
            }

        \item $W_2$ nie je jednotková klauzula -- vytvárame diferenčnú množinu
            $D_2 = \{ g(y), u \}$.

        \item $v_2 = u$, $t_2 = g(y)$.

        \item \itemMath{ 
            \begin{align*}
            \sigma_3 &= \sigma_2 \circ \{t_2/v_2\}
                = \{a/z, f(a)/x\} \circ \{g(y)/u\}
                = \{a/z,\ f(a)/x,\ g(y)/u\} \\[5pt]
            \begin{split}
                W_3 &= W_2 \{ t_x/v_2\} = 
                    \{ P(a,f(a),f(g(y))),\ P(a,f(a),f(u))\} \{g(y)/u\} = \\
                    &= \{ P(a,f(a),f(g(y))),\ f(a,f(a),f(g(y)) \}
            \end{split}
            \end{align*}
            }

        \item $W_3$ obsahuje iba jedinú klauzulu a teda
            $\sigma_3$ je najvšeobecnejší unifikátor pre množinu klauzúl $W$.
    \end{enumerate}
\end{priklad}


\begin{priklad}
    Zistite, či je unifikovateľná množina 
    \begin{equation*}
        W=\{Q(f(a),g(x)),\ Q(y,y)\}
    \end{equation*}

    \begin{enumerate}
    \item $\sigma_0 = \eps$, $W_0 = W$.

    \item $W_0$ obsahuje viac klauzúl.
        Nájdeme diferenčnú množinu $D_0 = \{f(a), y \}$.

    \item $v_1=y$, $t_1=f(a)$.

    \item $\sigma_1 = \sigma_0 \circ \{ t_0/v_0\} = 
                \eps \circ  \{f(a)/y\} = \{f(a)/y\}$.

    \item $W_1 = W_0 \{ t_0/\sigma_0\} = \{ Q(f(a),g(x)),\
        Q(f(a),f(a))\}$.

    \item $W_1$ obsahuje 2 klauzuly,
        zostrojujeme $D_1 = \{g(x), f(a)\}$.

    \item V $D_1$ nemáme prvok, ktorý by bol premennou.
        Algoritmus ukončí svoju činnosť s výsledkom, že
        $W$ nie je unifikovateľná.
    \end{enumerate}
\end{priklad}

\begin{poznamka}
    Pri zisťovaní unifikovateľnosti vždy vytvárame množiny $W_i$ tvaru
    \begin{equation*}
        W\sigma_0, W\sigma_1, W\sigma_2, \dots
    \end{equation*}
    pričom v každom kroku sa zmenší počet premenných aspoň o 1.
    Po konečnom počte krokov sa teda algoritmus musí zastaviť.
\end{poznamka}

\begin{veta}[Unifikačná]
    Ak $W$ je konečná neprádzna unifikovateľná množina výrazov,
    tak unifikačný algoritmus vždy zakončuje svoju činnosť na druhom kroku
    a posledné $\sigma_k$ je najvšeobecnejší unifikátor.
\end{veta}

\begin{dokaz}
    Nech $W$ je unifikovateľná množina a nech $\Theta$ označuje jej
    ľubovoľný unifikátor.
    Označme si počet kôl algoritmu ako $n$.
    
    Indukciou ukážeme, že pre každé kolo $k$ počas výpočtu programu existuje
    taká substitácia $\lambda_k$, že $\Theta = \sigma_k \circ \lambda_k$.

    \begin{itemize}
    \item Báza indukcie: Nech $k = 0$. Máme ukázať, že existuje
    $\lambda_0$, pre ktorú platí $\Theta = \sigma_0 \circ \lambda_0$.
    V tomto prípade $\sigma_0 = \varepsilon$ a teda $\lambda_0 = \Theta$.

    \item Indukčný krok: Predpokladáme, že existuje $\lambda_k$, 
        pre ktoré platí $\Theta = \sigma_k \circ \lambda_k$.
        Pozrime sa na množinu $W_{k+1}= W\sigma_{k+1}$.

        Ak $W_k$ je jednotková klauzula, tak algoritmus zakončuje 
        svoju činnosť na druhom kroku a $\sigma_k$ je
        najvšeobecnejší unifikátor pre $W$. 

        Nech teda $W_k$ nie je jednotková množina.
        Potom hľadáme diferenčnú množinu $D_k$ pre množinu $W_k$. 
        $D_k$ je diferenčná množina pre $W_k$ a 
        vo $W_k$ musí existovať premenná -- označme ju $v_k$. 
        Ďalej musí existovať term $t_k$ rôzny od $v_k$.
        Ak by toto neplatilo, tak množina by nemohla byť
        unifikovateľná.\footnote{Náhľad prečo: Vieme, že
            $\Theta = \sigma_k \circ \lambda_k$ a pre $\lambda_k$ musí
            nutne unifikovať diferenčnú množinu $D_k$. Tým pádom aspoň
            jedna z ``jednotkových substitúcii'' v $\lambda_k$ musí
            obsahovať elementy z $D_k$.
        }

        Vieme, že diferenčnú množinu $D_k$ unifikuje substitúcia $\lambda_k$.
        Teda $v_k \lambda_k = t_k \lambda_k$.

        Ďalej budeme potrebovať, že $v_k$ nie je obsiahnuté v $t_k$.
        Ak by totiž premenná $v_k$ bola obsiahnutá v $t_k$, dôjdeme k sporu.
        Platilo by aj ``$v_k \lambda_k$ je obsiahnutá v 
        $t_k \lambda_k$''. Lenže vieme, že tam platí rovnosť a preto by
        musela platiť aj rovnosť $v_k=t_k$. Spor.

        Vypočítame $\sigma_{k+1}=\sigma_k \circ \{t_k/v_k\}$.
        Potrebovali by sme nájsť $\lambda_{k+1}$. Môžeme si ho
        napríklad ``tipnúť'' ako 
        $\lambda_{k+1} = \lambda_k - \{t_k\lambda_k/v_k\}$. 

        Pretože $v_k$ sa nevyskytuje v $t_k$, platí
        $t_k \{ t_k\lambda_k / v_k\} = \eps$ a tým pádom
        \begin{equation*}
            t_k \lambda_{k+1} = t_k (\lambda_k - \{t_k\lambda_k / v_k\}) 
            =t_k \lambda_k
        \end{equation*}
        A teda dostávame
        \begin{equation*}
        \begin{split}
            \{ t_k / v_k\} \circ \lambda_{k+1} &= 
            \{t_k \lambda_{k+1}/v_k \} \union \lambda_{k+1} \\
            & = \{t_k \lambda_k/v_k \} \union \lambda_{k+1} \\
            & = \{t_k \lambda_k/v_k\} \union 
                ( \lambda_k - \{ t_k\lambda_k/v_k\}) \\ 
            &= \lambda_k
        \end{split}
        \end{equation*}

        Výsledok je teda, že 
        $\lambda_{k} = \{ t_k / v_k \} \circ \lambda_{k+1}$,
        čiže $\Theta = \sigma_k \circ \lambda_k
            = \sigma_k \circ \{t_k/v_k\} \circ \lambda_{k+1}
            = \sigma_{k+1} \circ \lambda_{k+1}$. A to sme chceli
            ukázať.
    \end{itemize}
\end{dokaz}
